feat(Lorentz.Vector): mark Vector and CoVector implicit_reducible, add inner_eq_sum - #1610
Conversation
…eq_sum `Lorentz.Vector` and `Lorentz.CoVector` are plain `def`s applied directly as functions throughout the library. Under Lean 4.33's `backward.isDefEq.respectTransparency.types` such applications are not type-correct at implicit transparency, which stops `rw`/`simp` matching patterns containing them. Marking both `@[implicit_reducible]` is the fix recommended by the release notes. Adds `inner_eq_sum` for both types; `basis_inner`/`inner_basis` are reproved from it, and the `erw`s in `basis_apply`/`basis_repr_apply` become plain `rw`. In total 21 `respectTransparency` options become unnecessary (2 in Vector/Basic, 19 in the Vector/CoVector tensorial, representation and contraction files) and are removed. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The `-Fintype.sum_sum_type` exclusions in `inner_eq_sum`, `basis_inner` and `inner_basis` were unnecessary. `CoVector.equivEuclid_apply` mirrors the existing `Vector.equivEuclid_apply` simp lemma, which removes the manual `rfl` from `CoVector.inner_eq_sum`. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The Euclidean inner product on `CoVector` has no consumers in the library, so these lemmas were speculative API. `CoVector` keeps only the `implicit_reducible` attribute, the `erw` removals and the docstring fix. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
| implicit-reducible lets such applications typecheck at implicit transparency, so that | ||
| `rw` and `simp` can match patterns containing them (see the Lean 4.33 release notes on | ||
| `backward.isDefEq.respectTransparency.types`). -/ | ||
| attribute [implicit_reducible] Vector |
There was a problem hiding this comment.
Would it not be better to do
@[implicit_reducible]
def Vector .... There was a problem hiding this comment.
fixed, wondering if it's a good idea to keep the explanation in or remove them
There was a problem hiding this comment.
Think it would be nice to keep it somewhere
jstoobysmith
added
the
awaiting-author
|
-awaiting-author |
github-actions
Bot
removed
the
awaiting-author
2 participants
Lorentz.Vector dandLorentz.CoVector dare defs forFin 1 ⊕ Fin d → ℝand are applied directly as functions throughout the library (v μ, x (Sum.inl 0), …). Lean 4.33 enablesbackward.isDefEq.respectTransparency.typesby default, under which such applications are not type-correct at implicit transparency (the note "function expected v μ" in error messages). Once a goal contains one under a binder,rwandsimpcan fail to match patterns that are visibly present. The release notes recommend marking the definitions involved@[implicit_reducible]; this PR does that for both types.Lorentz.Vector.inner_eq_sumis added to simplify proofs previously going through equivEuclid, WithLp and PiLp.as a result, all
set_option backward.isDefEq.respectTransparency falseand occurences oferwin these files can be removedPR drafted by claude and finalised by myself